$\forall$$T$:Type, $r$, ${\it r'}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$), $a$, $b$:$T$. ($r$ $\Lleftarrow\!\Rrightarrow$\{$T$\} ${\it r'}$) $\Rightarrow$ (($a$ [$r$] $b$) $\Leftarrow\!\Rightarrow$ ($a$ [${\it r'}$] $b$))